((v1 v1 9) (v2 v3 9))
38
()